Nuprl Lemma : pair-inherence
0,22
postcript
pdf
A
,
B
:Type,
x
:
A
,
y
:
B
,
a
:Atom1.
AtomFree(Type;
A
)
AtomFree(Type;
B
)
(<
x
,
y
>:
A
B
>>
a
x
:
A
>>
a
y
:
B
>>
a
)
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
,
t
T
,
Prop
,
x
:
T
>>
a
,
{
T
}
,
x
:
A
.
B
(
x
)
,
A
,
False
Lemmas
inheres
wf
,
atom-free
wf
,
assert
wf
,
matters
wf
origin
A, B:Type, x:A, y:B, a:Atom1.
AtomFree(Type;B) (<x,y>:A
B>>a 
x:A>>a 
y:B>>a) A, B:Type, x:A, y:B, a:Atom1.
AtomFree(Type;B) (<x,y>:AB>>a x:A>>a y:B>>a) x:A. B(x) Q Q Q Q
T
x:A. B(x)
A